public class FindDuplicate {
    
    public static void main (String[] args) {	
      	System.out.println(findDuplicate(args));	
    }
    
    
    /*
     * For this one we will need three "cases".
     * Case 1: If the length of arr is zero this implies there are no strings,
     * nothing to compare with and it will return null.
     * 
     * Case 2: If there are strings in arr (length > 0) We start the walkthrough
     * of strings in tab to find if there is a duplicate, we constantly add the
     * strings to the tab in order to find possible duplicates.
     * 
     * Case 3: If there are strings in arr (length > 0) We start the walk through
     * of strings in tab to find if there is a duplicate. If we do not find any 
     * string in arr which is a duplicate we return null. 
     * 
     * ************************************************************************
     * So we need three ensures here, one if the return is null (caused by 
     * length == 0), one if the return is a duplicate and one if we have length>0
     * but we find no duplicate return null. 
     * This gives us three requires as well, one length == 0, 
     * ************************************************************************
     * 
     */

   /*@ public normal_behavior
     @  requires arr.length ==0;
     @ ensures \result == null;
     @
     @ also
     @
     @ requires arr.length >0;
     @ ensures \result == null ==> 
     @ (\forall int i,j; i>=0 && i<arr.length && j>=0 && j <arr.length;
     @ !arr[i].equals(arr[j]));
     @
     @ also
     @
     @ requires arr.length >0;
     @ ensures \result !=null ==>
     @ ((\exists int i,j; i>=0 && i<arr.length && j>=0 && j <arr.length;
     @ arr[i].equals(arr[j]) && arr[i] == \result));
     @
     @*/
    
    
    // The last one may be done using an exist instead of a result != null.
    // Not completely sure if it matters.
    //test for exist instead: 
    /* requires arr.length >0;
     * ensures (\result != null ==> (\exists int i; i>=0 && i<arr.length;
     * arr[i].equals(arr[j]) && arr[i] == \result));
     */

    public static String findDuplicate(String[] arr) {
	
    	  HashTable tab = new HashTable( 100 );
	
      	for ( int i = 0; i < arr.length; i++ ) {
	          if ( tab.contains( arr[i] ) )
            		return arr[i];	    
      	    tab.add( arr[i] );
      	}
      	
      	return null;
    }
    
}